/*
Copyright 2007 Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato

    This file is part of KLMLean.

    KLMLean is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    KLMLean is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with KLMLean.  If not, see <http://www.gnu.org/licenses/>.
*/


/* Theorem prover for KLM Rational logic R - free variables version */
:- op(400,xfy,<), 
   op(400,fy,neg), 
   op(400,fy,box),
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,xfy,=>).
:-use_module(library(lists)).
:-use_module(library(clpfd)).


/* --------------------------------------------------------------------------------------- */

/* The following predicate implements the calculi:

    prove(Gamma,1,[],Tree) iff there exists a closed tableaux Tree for Gamma
    
    [Y,<,X] is used to represent that Y < X 
    Lables are represented by integers starting from 1
    
    In prove(Gamma,Max,Cond,Tree) we have that:
    - Max is the last label introduced in the current branch (the maximum integer in the branch)
    - Cond is a list of pairs [A => B,Used], where Used is a list of free variables,
      representing that the (|~+) rule has already been applied in the current branch by
      introducing the labels in Used. 
      In order to ensure termination, (|~+) is applied to A=> B only if the cardinality of Used,
      i.e. the number of free variables already used to apply the rule to A => B in the current branch, 
      is < than Max. The predicate all_different is used in order to ensure that all free variables
      in Used assume different values (it is useless to apply (|~+) more than once in the same world in
      each branch of a proof tree)
     
    
*/

prove(Gamma,_,_,tree(axiom)):-member([X,F],Gamma),member([X,neg F],Gamma),!.

prove(Gamma,_,_,tree(axiom)):-member([X,<,Y],Gamma),member([Y,<,X],Gamma),!.

prove(Gamma,Max,Cond,tree(neg,[X,neg neg A],SubTree)):-
  select([X,neg neg A],Gamma,NewGamma),!,
  prove([[X,A]|NewGamma],Max,Cond,SubTree).

prove(Gamma,Max,Cond,tree(andP,[X,A and B],SubTree)):-
  select([X,A and B],Gamma,NewGamma),!,
  prove([[X,A]|[[X,B]|NewGamma]],Max,Cond,SubTree).
  
prove(Gamma,Max,Cond,tree(impN,[X,neg (A -> B)],SubTree)):-
  select([X,neg (A -> B)],Gamma,NewGamma),!,
  prove([[X,A]|[[X,neg B]|NewGamma]],Max,Cond,SubTree).
  
prove(Gamma,Max,Cond,tree(orN,[X,neg (A or B)],SubTree)):-
  select([X,neg (A or B)],Gamma,NewGamma),!,
  prove([[X,neg A]|[[X,neg B]|NewGamma]],Max,Cond,SubTree).
   
prove(Gamma,Max,Cond,tree(orP,[X,A or B],LeftTree,RightTree)):-
  select([X,A or B],Gamma,NewGamma),!,
  prove([[X,A]|NewGamma],Max,Cond,LeftTree),
  prove([[X,B]|NewGamma],Max,Cond,RightTree).

prove(Gamma,Max,Cond,tree(andN,[X,neg (A and B)],LeftTree,RightTree)):-
  select([X,neg (A and B)],Gamma,NewGamma),!,
  prove([[X,neg A]|NewGamma],Max,Cond,LeftTree),
  prove([[X,neg B]|NewGamma],Max,Cond,RightTree).
  
prove(Gamma,Max,Cond,tree(impP,[X,A -> B],LeftTree,RightTree)):-
  select([X,A -> B],Gamma,NewGamma),!,
  prove([[X,neg A]|NewGamma],Max,Cond,LeftTree),
  prove([[X,B]|NewGamma],Max,Cond,RightTree).

prove(Gamma,Max,Cond,tree(<,[X,<,Y],Z,LeftTree,RightTree)):-
  member([X,<,Y],Gamma),
  Z in 1..Max,
  X#\=Z,
  Y#\=Z,
  \+member([X,<,Z],Gamma),
  \+member([Z,<,Y],Gamma),
  labeling([],[Y,Z]),
  gammaM(Gamma,Y,Z,ResLeft),
  gammaM(Gamma,Z,X,ResRight),
  append(ResLeft,Gamma,LeftConcl),
  append(ResRight,Gamma,RightConcl),
  prove([[Z,<,Y]|LeftConcl],Max,Cond,LeftTree),
  prove([[X,<,Z]|RightConcl],Max,Cond,RightTree).

prove(Gamma,Max,Cond,tree(condN,[U,neg(A => B)],X,SubTree)):-
  select([U,neg (A => B)],Gamma,NewGamma),!,
  X#=Max+1,
  prove([[X,A]|[[X,box neg A]|[[X,neg B]|NewGamma]]],X,Cond,SubTree).
  

prove(Gamma,Max,Cond,tree(boxN,[X,neg box neg A],Y,SubTree)):-
  select([X,neg box neg A],Gamma,NewGamma),!,
  Y#=Max+1,
  labeling([],[X]),
  gammaM(NewGamma,X,Y,GammaM),
  append(NewGamma,GammaM,GammaConclusion),
  prove([[Y,<,X]|[[Y,box neg A]|[[Y,A]|GammaConclusion]]],Y,Cond,SubTree).


prove(Gamma,Max,Cond,tree(condP,[Y,A => B],LeftTree,RightTree)):-
  member([_,A => B],Gamma),
  \+member([A => B,_],Cond),!,
  Y in 1..Max,
  prove([[Y,A -> B]|Gamma],Max,[[A => B,[Y]]|Cond],LeftTree),
  prove([[Y,neg box neg A]|Gamma],Max,[[A => B,[Y]]|Cond],RightTree).
  
prove(Gamma,Max,Cond,tree(condP,[Y,A => B],LeftTree,RightTree)):-
  member([_,A => B],Gamma),
  select([A => B,Used],Cond,NewCond),
  length(Used,N),
  N<Max,!,
  Y in 1..Max,
  all_different([Y|Used]),
  prove([[Y,A -> B]|Gamma],Max,[[A => B,[Y|Used]]|NewCond],LeftTree),
  prove([[Y,neg box neg A]|Gamma],Max,[[A => B,[Y|Used]]|NewCond],RightTree).


/* Auxiliary predicate computing \Gamma^M_{x -> y} */
gammaM([],_,_,[]):-!.
gammaM([[X,box A]|Tail],X,Y,[[Y,A]|[[Y,box A]|ResTail]]):-!,gammaM(Tail,X,Y,ResTail).
gammaM([_|Tail],X,Y,ResTail):-gammaM(Tail,X,Y,ResTail).



/* --------------------------------------------------------------------------------------- */

/* The following predicate builds a model for a satisfiable set of formulas:

    proveCounter(Gamma,[],[]) 
    
*/


proveCounter(Gamma,_,_,_):-member([X,F],Gamma),member([X,neg F],Gamma),!.

proveCounter(Gamma,_,_,_):-member([X,<,Y],Gamma),member([Y,<,X],Gamma),!.

proveCounter(Gamma,Cond,Labels,Max):-
  select([X,neg neg A],Gamma,NewGamma),!,
  proveCounter([[X,A]|NewGamma],Cond,Labels,Max).

proveCounter(Gamma,Cond,Labels,Max):-
  select([X,A and B],Gamma,NewGamma),!,
  proveCounter([[X,A]|[[X,B]|NewGamma]],Cond,Labels,Max).
  
proveCounter(Gamma,Cond,Labels,Max):-
  select([X,neg (A -> B)],Gamma,NewGamma),!,
  proveCounter([[X,A]|[[X,neg B]|NewGamma]],Cond,Labels,Max).
  
proveCounter(Gamma,Cond,Labels,Max):-
  select([X,neg (A or B)],Gamma,NewGamma),!,
  proveCounter([[X,neg A]|[[X,neg B]|NewGamma]],Cond,Labels,Max).

proveCounter(Gamma,Cond,Labels,Max):-
  select([X,A or B],Gamma,NewGamma),!,
  proveCounter([[X,A]|NewGamma],Cond,Labels,Max),!,
  proveCounter([[X,B]|NewGamma],Cond,Labels,Max).

proveCounter(Gamma,Cond,Labels,Max):-
  select([X,neg (A and B)],Gamma,NewGamma),!,
  proveCounter([[X,neg A]|NewGamma],Cond,Labels,Max),!,
  proveCounter([[X,neg B]|NewGamma],Cond,Labels,Max).
  
proveCounter(Gamma,Cond,Labels,Max):-
  select([X,A -> B],Gamma,NewGamma),!,
  proveCounter([[X,neg A]|NewGamma],Cond,Labels,Max),!,
  proveCounter([[X,B]|NewGamma],Cond,Labels,Max).

proveCounter(Gamma,Cond,Labels,Max):-
  member([X,<,Y],Gamma),
  member(Z,Labels),
  X\=Z,
  Y\=Z,
  \+member([X,<,Z],Gamma),
  \+member([Z,<,Y],Gamma),!,
  gammaM(Gamma,Y,Z,ResLeft),
  gammaM(Gamma,Z,X,ResRight),
  append(ResLeft,Gamma,LeftConcl),
  append(ResRight,Gamma,RightConcl),
  proveCounter([[Z,<,Y]|LeftConcl],Cond,Labels,Max),!,
  proveCounter([[X,<,Z]|RightConcl],Cond,Labels,Max).

proveCounter(Gamma,Cond,Labels,Max):-
  select([_,neg (A => B)],Gamma,NewGamma),!,
  X is Max+1,!,
  proveCounter([[X,A]|[[X,box neg A]|[[X,neg B]|NewGamma]]],Cond,[X|Labels],X).
  
proveCounter(Gamma,Cond,Labels,Max):-
  select([X,neg box neg A],Gamma,NewGamma),!,
  Y is Max+1,!,
  gammaM(NewGamma,X,Y,GammaM),
  append(NewGamma,GammaM,GammaConclusion),
  proveCounter([[Y,<,X]|[[Y,box neg A]|[[Y,A]|GammaConclusion]]],Cond,[Y|Labels],Y).

proveCounter(Gamma,Cond,Labels,Max):-  
  member([_,A => B],Gamma),
  \+member([A => B,_],Cond),!,
  member(U,Labels),
  proveCounter([[U,A -> B]|Gamma],[[A => B,[U]]|Cond],Labels,Max),!,
  proveCounter([[U,neg box neg A]|Gamma],[[A => B,[U]]|Cond],Labels,Max).
  
proveCounter(Gamma,Cond,Labels,Max):-
  member([_,A => B],Gamma),
  select([A => B,Used],Cond,NewCond),
  member(U,Labels),
  \+member(U,Used),!,
  proveCounter([[U,A -> B]|Gamma],[[A => B,[U|Used]]|NewCond],Labels,Max),!,
  proveCounter([[U,neg box neg A]|Gamma],[[A => B,[U|Used]]|NewCond],Labels,Max).  

proveCounter(Gamma,_,Labels,_):-
  listOfAtoms(Gamma,Temp),
  listOfTransitions(Gamma,TempTrans),
  remove_duplicates(Temp,Atoms),
  transitivityOfRelation(TempTrans,OtherTransitions),
  append(TempTrans,OtherTransitions,Transitions),
  remove_duplicates(Gamma,Ext),
  throw(saturatedBranch(Atoms,Labels,Transitions,Ext)).

/* Given a list of formulas, returns the list of atoms */
listOfAtoms([],[]):-!.
listOfAtoms([[X,A]|Tail],[[X,A]|ResTail]):-atom(A),!,listOfAtoms(Tail,ResTail).
listOfAtoms([_|Tail],ResTail):-!,listOfAtoms(Tail,ResTail).

/* Given a list of formulas, returns the list of transitions (=values of the modular relation) */
listOfTransitions([],[]):-!.
listOfTransitions([[X,<,Y]|Tail],[[X,<,Y]|ResTail]):-!,listOfTransitions(Tail,ResTail).
listOfTransitions([_|Tail],ResTail):-!,listOfTransitions(Tail,ResTail).


/* Transitive closure of the preference relation */
transitivityOfRelation(List,[]).
  

/* Top-level predicates, also used to build a countermodel in case the initial
   set of formulas is satisfiable */
nmcr(K,F,Tree):-parseinput([F|K]),label(K,LabK),
  ((prove([[1,neg F]|LabK],1,[],Tree),!)
  ;
  catch(proveCounter([[1,neg F]|LabK],[],[1],1),saturatedBranch(Atoms,Max,Transitions,Gamma),
  canonicalModel(Atoms,Max,Transitions,Gamma,Tree))
  ).

canonicalModel(Atoms,Labels,Transitions,Gamma,model(Atoms,Labels,Transitions,Gamma)).  
  
unsatinterface(K,[F],Tree):-parseinput([F|K]),label(K,LabK),prove([[1,neg F]|LabK],1,[],Tree).
unsatinterface(K,[],Tree):-parseinput(K),label(K,LabK),prove(LabK,1,[],Tree).

countermodel(K,[F],Model):-parseinput([F|K]),label(K,LabK),
  catch(proveCounter([[1,neg F]|LabK],[],[1],1),saturatedBranch(Atoms,Labels,Transitions,Gamma),
  canonicalModel(Atoms,Labels,Transitions,Gamma,Model)).
countermodel(K,[],Model):-parseinput(K),label(K,LabK),
  catch(proveCounter(LabK,[],[1],1),saturatedBranch(Atoms,Labels,Transitions,Gamma),
  canonicalModel(Atoms,Labels,Transitions,Gamma,Model)).




/* Predicate used to control that the inserted formula belongs to the language LR of R logic:

  - propositional formulas belong to LR
  - if A and B are propositionals, then A => B belongs to LR
  - a boolean combination F of formulas of LR belongs to LR
  
*/

parseinput([]):-!.
parseinput([F|Tail]):-parse(F),parseinput(Tail).

parse(P):-atom(P).
parse(F and G):-parse(F),parse(G).
parse(F or G):-parse(F),parse(G).
parse(F -> G):-parse(F),parse(G).
parse(neg F):-parse(F).
parse(A => B):-boolcomb(A),boolcomb(B).

boolcomb(P):-atom(P).
boolcomb(A and B):-boolcomb(A),boolcomb(B).
boolcomb(A or B):-boolcomb(A),boolcomb(B).
boolcomb(A -> B):-boolcomb(A),boolcomb(B).
boolcomb(neg A):-boolcomb(A).


/* Predicates used to reconstruct the proof tree or the model (used by the GUI) */
javaTree(tree(axiom),Node,jT(ax,Node,null,null)):-!.


javaTree(tree(andP,[X,A and B],Sub),Node,jT(andP,Node,SubJava,null)):-!,
  select([X,A and B],Node,Temp),
  javaTree(Sub,[[X,A]|[[X,B]|Temp]],SubJava).
  
javaTree(tree(andN,[X,neg (A and B)],S1,S2),Node,jT(andN,Node,SJ1,SJ2)):-!,
  select([X,neg (A and B)],Node,Temp),
  javaTree(S1,[[X,neg A]|Temp],SJ1),
  javaTree(S2,[[X,neg B]|Temp],SJ2).  
  
javaTree(tree(orP,[X,A or B],S1,S2),Node,jT(orP,Node,SJ1,SJ2)):-!,
  select([X,A or B],Node,Temp),
  javaTree(S1,[[X,A]|Temp],SJ1),  
  javaTree(S2,[[X,B]|Temp],SJ2).
  
javaTree(tree(orN,[X,neg (A or B)],Sub),Node,jT(orN,Node,SubJava,null)):-!, 
  select([X,neg (A or B)],Node,Temp), 
  javaTree(Sub,[[X,neg A]|[[X,neg B]|Temp]],SubJava).
  
javaTree(tree(impP,[X,A -> B],S1,S2),Node,jT(impP,Node,SJ1,SJ2)):-!,
  select([X,A -> B],Node,Temp),
  javaTree(S1,[[X,neg A]|Temp],SJ1),
  javaTree(S2,[[X,B]|Temp],SJ2).
 
javaTree(tree(neg,[X, neg neg A],Sub),Node,jT(neg,Node,SubJava,null)):-!,
  select([X,neg neg A],Node,Temp),
  javaTree(Sub,[[X,A]|Temp],SubJava).

javaTree(tree(impN,[X,neg (A -> B)],Sub),Node,jT(impN,Node,SubJava,null)):-!,   
  select([X,neg (A -> B)],Node,Temp),
  javaTree(Sub,[[X,A]|[[X,neg B]|Temp]],SubJava).
  

javaTree(tree(condN,[U,neg (A => B)],X,Sub),Node,jT(entN,Node,SubJava,null)):-!,  
  select([U,neg (A => B)],Node,Temp),
  javaTree(Sub,[[X,A]|[[X,box neg A]|[[X,neg B]|Temp]]],SubJava).  
  
javaTree(tree(boxN,[X,neg box neg A],Y,Sub),Node,jT(boxN,Node,SubJava,null)):-!,
  select([X,neg box neg A],Node,Temp),
  gammaM(Temp,X,Y,GammaM),
  append(Temp,GammaM,GammaConclusion),
  javaTree(Sub,[[Y,<,X]|[[Y,box neg A]|[[Y,A]|GammaConclusion]]],SubJava).

javaTree(tree(<,[X,<,Y],Z,LeftTree,RightTree),Node,jT(<,Node,SJ1,SJ2)):-!,
  gammaM(Node,Y,Z,ResLeft),
  gammaM(Node,Z,X,ResRight),
  append(ResLeft,Node,LeftConcl),
  append(ResRight,Node,RightConcl),
  javaTree(LeftTree,[[Z,<,Y]|LeftConcl],SJ1),
  javaTree(RightTree,[[X,<,Z]|RightConcl],SJ2).

 
javaTree(tree(condP,[U,A => B],S1,S2),Node,jT(entP,Node,SJ1,SJ2)):-!,
  javaTree(S1,[[U,A -> B]|Node],SJ1),  
  javaTree(S2,[[U,neg box neg A]|Node],SJ2).



/* Predicates used by the GUI to extract information about the closed tree */

getRule(jT(Rule,_,_,_),Rule):-!.
getNode(jT(_,Node,_,_),Node):-!.
getLeft(jT(_,_,Left,_),Left):-!.
getRight(jT(_,_,_,Right),Right):-!.

getAtoms(model(Atoms,_,_,_),Atoms):-!.
getLabels(model(_,Labels,_,_),Labels):-!.
getTransitions(model(_,_,Transitions,_),Transitions):-!.
getExtended(model(_,_,_,Extended),Extended):-!.


/* Given a list of formulas, returns the same list where formulas are labelled with 1 */
label([],[]):-!.
label([Formula|Tail],[[1,Formula]|ResTail]):-label(Tail,ResTail).
  
/* Given the number of labels, build the corresponding list of labels */
listOfLabels(1,[1]):-!.
listOfLabels(N,[N|Tail]):-N1 is N-1,listOfLabels(N1,Tail).